COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.if false then begin "questions"
C00004 00003	.s(EXTEND,TRANSFORMING LISP PROGRAMS)
C00007 00004	.ss(purify,Purifying LISP programs.)
C00021 00005	.ss(derive,Derived programs.)
C00036 00006	.ss(extendex,Substantial exercises)
C00037 ENDMK
C⊗;
.if false then begin "questions"

ref to Wegbreit w respect to derived programs

What about the fact that both the jmc and rww algorithms for
producing functional programs from sequential produce
more well defined functions in some cases.

	(PROG (X)
	  (SETQ X (FOO NIL))
	  (COND (T (RETURN T)) (T X)) )

converts to [if T then T else foo NIL]

and if foo NIL is undefined the later still has value T while the former 
is undefined.

.end "questions"

.if false then begin "notes"

This chapter should be converted to chapter on proving properties
of progs and other extensions to method and perhaps follow IMPURE

	u*[v*w] = [u*v]*w
but
	cost[u*[v*w]] ≤ cost[[u*v]*w]


Add example programs for some transformations.
    Clean
    Trace
Add exercises to do others.
    count conses
    recursion depth
    remove mapping functions from lisp term

.end "notes"
.s(EXTEND,TRANSFORMING LISP PROGRAMS)
.if NOTASSEMBLING then start
.ABSNTX: NEXT SECTION!;
.COMPIL: NEXT SECTION!;
.COMPUT: NEXT SECTION!;
.end

	The techniques developed in Chapter {SECTION PROVIN} were limited
to stating and proving extensional properties of functional LISP programs.
(Remember that extensional properties of programs are those that relate
the input and output).
Chapter {SECTION IMPURE} shows that non-functional LISP programs are also
useful.  Also many interesting properties of programs such as space or
time requirements, depth of recursion, number of calls to a particular function
during execution, etc., are not extensional.   In this chapter we show
how the first order techniques of Chapter {SECTION PROVIN} can be applied to a
larger class of problems.  In particular we discuss how to transform
certain sequential LISP programs into functional programs that compute the same 
function.  Thus extensional properties can be discussed in terms of the 
equivalent functional program.   
We also show how some intensional properties
can be handled by forming a "derived" program that computed the desired
property of the original program.  Finally we discuss briefly how 
to connect the formal properties of transforming programs with those of
the transformed programs using the ⊗meta theory of LISP.  This connection 
will allow us for example to
define intensional properties formally and show that the derived programs 
actually do compute the property correctly.
.ss(purify,Purifying LISP programs.)

	As we noted in Chapter {SECTION IMPURE} a sequential term occuring
as a term in a LISP program can be replaced by an extensionally equivalent
functional term under certain conditions.  A sufficient set of conditions
is the following:
.begin indent 4,8

1. All variables local to the program are initialized before being
used.  Of course, it could be taken as a convention that these variables
are initialized to qNIL when the program is entered.  Then it wouldn't
affect the correctness of the translation to a functional program if some
of them weren't further initialized.

2. All assignments are to variables local to the program.

3. Each label referred to in a qgo statement occurs exactly
once in the program.   
.end

	One method of finding a functional term equivalent to a sequential term 
is the following.  Suppose the qprog has local variables ⊗x1,...,xn.  
For each conditional branch (i.e. a conditional statement containing a qgo
or a qreturn) we define a new function.  If the conditional has the form

⊗⊗⊗qif p1 qthen s1 qelse qif ... qelse qif pn qthen sn⊗

then  the body of the function definition has the form 

⊗⊗⊗qif p1 qthen t1 qelse qif ... qelse qif pn qthen tn qelse t0⊗

where ⊗s0 is the sequence of statements following the conditional and
⊗ti is the result of executing the sequence of statements ⊗si;s0 
(or just ⊗s0  for ⊗t0 ) taking the current value of ⊗xi to be ⊗xi.  
We obtain the term corresponding to the result of executing a sequence of
statements as follows.  If the statement is an assigment then 
the current value of the variable becomes the current value of the term
on the right hand side. (The current value of the term is just the
term obtained by replacing all free occurrences of local variables
by their current values. If some local variable is needed that has no current
value then the current value of the term is undefined.) 
If the statement is a conditional without
any qgos or qreturns then it gets converted to a sequence of
assignments where the conditional has been distributed through the assignment.  
If the statement is a qgo
then the next statement to execute becomes the one with the corresponding
label.  If the next statement is a qreturn then the result is the current 
value of the term to be returned.  If the statement is one of the conditionals
for which we have created a new function then the result is that function
applied to the current values of the local variables.  If we are at the 
end of the list of statements then the result is undefined.
Finally the qprog term is replaced by the result of executing the
sequence of statements starting with the first, with the current values of
the local variables undefined.

	[In order to insure that this process will terminate we must keep
track of the labeled statements visited in an execution sequence so that
if a label gets visited twice unconditionally we know that this will be
an infinite loop and the result of executing this sequence will be defined.]

	As an example, consider the following expression that gives the
result of appending the list ⊗a with the reversal of ⊗a*b: 

⊗⊗⊗a*qprog[[u,v] u←a*b; v←qnil; loop: qif qn u qthen qreturn v; v←qa u . v; u←qd u;  qgo loop].⊗

This expression can be replaced by

⊗⊗⊗a * loop[a*b, qnil]                            ⊗

and the recursive definition

⊗⊗⊗loop[u,v] ← qif qn u qthen v qelse loop[d u,qa u . n].⊗

	A second method for transforming sequential terms into functional terms
is the following.  There will be a new function associated with each
label.  We process the list of statements in reverse order starting
with the last one and carry along a current result.  We begin with the result 
undefined.  If the statement just processed is labeled then we make the 
defining expression of the function corresponding to that label equal to the 
current result, and the current result becomes the corresponding function
applied to the list of local variables.
If we are at the top of the list then we are done and the
current result is the desired functional term.  If the next statement
is an assignment we replace all free occurrences of the assigned variable 
in the result by the expression part of the assignment.  
If the statement is a qreturn we replace the
result by the expression to be returned.  If the statement is a conditional
of the form 

⊗⊗⊗qif p1 qthen s1 qelse qif ... qelse qif pn qthen sn⊗

then the result is replaced by a conditional of the form 

⊗⊗⊗qif p1 qthen t1 qelse qif ... qelse qif pn qthen tn qelse t0⊗

where ⊗ti is the result of processing the statements ⊗si (bottom up)
starting with the current result (⊗t0 is just the current result).
If the statement is a qgo then the result is replaced by the application
of the function corresponding to the label to the list of local variables.

	The first method is based on the technique for transforming Flow Charts
or ALGOLic programs into recursive functional programs given in McCarthy[1962b]
The second technique for converting sequential programs into functional
programs was suggested by Richard Weyhrauch.  It is based on the general method
used by mathematical logicians to code informal descriptions of sequential 
computations into functional form (typically into λ-calculus).  
Both procedures give the
same result on the simple example given above as well as for the program
for ⊗append ({eqn appendprog3!!}) and a cleaned up version (adding an additional
local variable to eliminate assignments to a non local variable) of the
⊗reverse program ({eqn reverseprog!!}).

	The above conditions permit a purely local rewrite,  and they
are indeed unnecessarily restrictive.  The question is then how to
relax the restricitions in some useful way.  In any case
we must maintain the property that replacing an occurence of the sequential
term in an expression by its value  will not change the value of the expression.  
It seems evident that if an outer sequential program containing
an inner one satisfies the initialization and local assignment (i.e.
no side-effect) conditions, then the program can be converted to functional
form even if it contains sequential subprograms that violate these
conditions provided that all assignments in the inner program are at
least local to the outer program,  and that these inner programs can
be replaced by a functional term in such a way that the value of the
outer sequential term is not changed.  
The rules for doing this have not been formulated as yet.

	The reason for being particular about the kind of assignments allowed 
is that if a program should make assignments to external variables, 
ambiguities may arise.  Suppose we evaluate the expression

⊗⊗⊗<x, %3program%2[[] x ← qd x; qreturn x], x>.             ⊗

when ⊗x has the value $(A_B).  If the arguments of the list are "executed"
in left to right order, the expression will have value $((A_B)_(B)_(B)), 
whereas if the execution is from right to left, the value will be
$((B)_(B)_(A_B)).   However, the mathematical semantics of expressions
don't prescribe any order of evaluation, and experience with ALGOL_60,
which prescribed left-to-right evaluation in order to give a definite
meaning to function procedures that alter external variables, has shown
that the quality of compiled code is greatly reduced by prescribing
a fixed order.

	This ambiguity can be resolved by rewriting
expressions containing programs that change variables in the expression
using lambda expressions to force a desired order of evaluation.
Thus the above expression could be written

⊗⊗⊗[λy:[λz:<z,y,y>][qprog[[] x ← qd x; qreturn x]]][x]⊗

which would evaluate to $$((B)_(A_B)_(A_B))$ in the above case.  Seven other
results could be obtained by putting different combinations of ⊗z and ⊗y between
the pointy brackets.
Once these ambiguities have been resolved, it would seem that we could
translate an outer sequential program containing inner sequential
programs into a function program in a unique way even allowing the
inner programs to make assignments to variables in the outer programs.
The rules for doing this haven't been worked out, however.

.skip 2
.cb Exercises
.item←0
.group

	#. Write a LISP predicate that will determine whether a $PROG 
in internal form satisfies the above conditions for replacement by
a functional term.

	#. Given that a $PROG satisfies the conditions, write a LISP
functions to convert the $PROG expression and give the a list of the
required auxiliary function definitions.

.apart
.ss(derive,Derived programs.)

	So far we have discussed mainly extensional properties of programs.
Recall that an extensional property is a property that depends only on the
function computed by the program.   In many cases we would like to be able
to express and prove things about intensional properties such as space or
time requirements, depth of recursion, etc..  Thus the statement that
⊗⊗∀u.flatten_x=fringe_x⊗  expresses the extensional property that 
⊗flatten ({eqn flatten!!}) and ⊗fringe ({eqn fringe!!})
compute the same function.  However the statement 
made in Chapter {SECTION READIN} that ⊗flatten requires less computation than 
⊗fringe refers to an intensional property.  We could make this statement
more precise by saying that more ⊗⊗cons⊗es are executed in computing
⊗fringe_x than in computing ⊗flatten_x but the methods of Chapter {SECTION PROVIN}
do not allow us to prove it.

	Consider the problem of computing the number of ⊗⊗cons⊗es executed
when computing ⊗flatten_x.  Since ⊗flatten simply calls the auxiliary 
function ⊗flat we will do the problem for ⊗flat.  There are two cases.
If ⊗x is an atom then ⊗⊗flat[x,u]=x_._u⊗ so 1 ⊗cons is executed.
Otherwise ⊗⊗flat[x,u]=flat[qa x,flat[qd x,u]⊗ so the number of ⊗⊗cons⊗es
executed must be the sum of those executed in computing ⊗⊗flat[qd x,u]⊗ and
those executed ⊗⊗flat[qa x,v]⊗ where ⊗v is ⊗⊗flat[qd x,u]⊗.
The idea is to count the ⊗⊗cons⊗es executed in computing the values of the
arguments and add to that the number of ⊗⊗cons⊗ executed in computing
the program with those values as arguments.  Thus we can define the function
⊗cflat that computes the number of ⊗⊗cons⊗es executed in computing ⊗flat by
.begin nofill group select 2 turnon"∂"
.n←20

∂(n)cflat[x, u] ← 
!fcncflat& ∂(n+4)qif qat x qthen $$1$ 
∂(n+4)qelse cflat[qa x, flat[qd x, u]] + cflat[qd x, u]
.end

for example
.begin nofill group

⊗⊗⊗cflat[$$(A . (B . (C . D)))$, qNIL] = $$4$⊗
⊗⊗⊗cflat[$$(((A . B) . C) . D)$, qNIL] = $$4$⊗
.end
We can express the function computed by ⊗cflat in terms of the
size of the input using ⊗size ({eqn size2!!}) by

!eqncflatval ⊗⊗⊗∀x u: cflat[x, u] = size x⊗.

To prove this statement we us S-expresion induction on ⊗x.  
In the case ⊗x is an atom ⊗⊗∀u.cflat[x,u]=$$1$=sixe_x⊗ by simplifying the 
definitions.  Otherwise we may assume ⊗⊗∀u.cflat[qa x,u]=size_qa x⊗ and
⊗⊗∀u.cflat[qd x,u]=size_qd x⊗ .  Now 
.begin nofill group turnon "∂" 
.n←12; m←20; i←56

∂(n)⊗⊗cflat[x,u]∂(m)=cflat[qa x,flat[qd x,u]]+cflat[qd x,u]⊗∂(i)definition of ⊗flat 
              ∂(m)⊗⊗=size qa x + size qd x⊗∂(i)induction hypothesis
	      ∂(m)⊗⊗=size x⊗∂(i)definition of ⊗size 
.end
Notice that in order to make the second step we need to know that ⊗flat is
total.

	Now we will do the same construction for ⊗fringe.  When ⊗x is
an atom then ⊗⊗fringe_x=x_._qNIL⊗ so the number of ⊗⊗cons⊗es is $1. 
Otherwise ⊗⊗fringe_x=fringe_qa x_*_fringe_qd x⊗.  So we count the number
of ⊗⊗cons⊗es executed in computing ⊗⊗fringe_qa x⊗ and  ⊗⊗fringe_qd x⊗ and
add to this the number executed in computing ⊗⊗u_*_v⊗ where ⊗u is
⊗⊗fringe_qa x⊗ and ⊗v is ⊗⊗fringe_qd x⊗.  A similar analysis can be made 
for ⊗append.  Thus we can define the functions
⊗cfringe and ⊗cappend by
.begin nofill group turnon"∂" select 2
.n←20

∂(n)cfringe x ← 
!fcncfringe& ∂(n+4)qif qat x qthen $$1$
∂(n+4)qelse cappend[fringe qa x, fringe qd x] + cfringe qa x + cfringe qd x
%1and%*
∂(n)cappend[u,v] ← 
!fcncappend& ∂(n+4)qif qn u qthen $0 qelse $1 + cappend[qd u, v]
.end

For example
.begin nofill group

⊗⊗⊗cfringe[$$(A . (B . (C . D)))$] = $$7$⊗
⊗⊗⊗cfringe[$$(((A . B) . C) . D)$] = $$10$⊗
.end
We can express ⊗cfringe in terms of the size of the input  by
.begin nofill group

⊗⊗⊗∀x: cfringe x ≥ $2 q* size x - $$1$⊗
!eqncfringeval 
⊗⊗⊗∀x: [size x + $$1$]q*[size x] ≥ $2 q* cfringe x⊗
.end
This can be proved by S-expression using the fact that 

!eqncappfringe ⊗⊗⊗∀x u.cappend[fringe x,u]=size x⊗.

In the case ⊗x is atomic the inequalities reduce to 1≥1 and 2≥2 using
the function definitions.  Otherwise we have
.begin nofill group turnon "∂"
.n←12 m←20 i←56

∂(n)⊗⊗cfringe x ∂(m)= cappend[fringe qa x,fringe qd x]⊗
		∂(m)⊗⊗  + cfringe qa x + cfringe qd x ⊗∂(i)by definition of ⊗cfringe  
		∂(m)⊗⊗≥ cappend[fringe qa x,fringe qd x]⊗
		∂(m)⊗⊗  + $$2$q*[size qa x-$$1$] + $$2$q*[size qd x-$$1$]⊗∂(i)by induction
		∂(m)⊗⊗≥ size qa x + $$2$q*[size x-$$2$]⊗∂(i) by definition of ⊗size and {eqn cappfringe!}
		∂(m)⊗⊗≥ $$2$q*[size x-$$1$]⊗∂(i) since ⊗⊗size qa x⊗≥$$1$
.end
and
.begin nofill group turnon "∂"
.n←12 m←20 i←54

∂(n-2)⊗⊗$$2$q*cfringe x ∂(m)= $$2$q*[cappend[fringe qa x,fringe qd x]⊗
		∂(m)⊗⊗  + cfringe qa x + cfringe qd x]⊗∂(i)by definition of ⊗cfringe  
		∂(m)⊗⊗≤ $$2$q*size qa x ⊗
		∂(m)⊗⊗  + [size qa x+$$1$]q*[size qa x]⊗
		∂(m)⊗⊗  + [size qd x+$$1$]q*[size qd x]⊗∂(i)by induction and {eqn cappfringe!}
		∂(m)⊗⊗≤ [sixe qa x+size qd x+$$1$]q*[size qa+size qd x]⊗∂(i)by computation
		∂(m)⊗⊗≤ [sixe x+$$1$]q*[size x]⊗∂(i)by definition of ⊗size 
.end
Thus with the aid of the derived programs ⊗cflat and ⊗cfringe we are able
to make a quantitative comparison of the amount of computation done by
⊗flat and ⊗fringe.  

	The derived program that computes the number of ⊗⊗cons⊗es executed
in computing a program is an example of a general class of ⊗cost computing
derived programs.  The rules for obtaining such a derived program from
the original program definition are as follows.  First associate a
cost program with each of the function applications occuring in defining 
expression.  (This includes associating the program to be derived with the 
original program.)  Then transform the defining expression.   If the
expression is a constant or variable then the cost is $0.  If the expression
is a conditional of the form 

⊗⊗⊗qif p qthen tq1 qelse tq2⊗ 

then it is transformed into

⊗⊗⊗<cost(p)>+qif p qthen <cost(tq1)> qelse <cost(tq2)>⊗.

where ⊗⊗<cost(e)>⊗ is the cost term derived by applying the rules to 
to ⊗e.  
If the expression is a list forming operation we replace it by the equivalent
composition of ⊗⊗cons⊗es and then proceed as usual.
If the expression is the application of a function, ⊗f, to a list of arguments
then it is transformed into the sum of the costs of the arguments plus
the cost function corresponding to ⊗f applied to the argument values.
If the expression is a lambda expression applied to a list of arguments
it is transformed into the sum of the costs of the arguments plus the
cost of the body of the lambda expression. 

	Thus if we put ⊗⊗ccons[x,y]←$$1$⊗ and all other cost functions
except ⊗cflat equal to the zero function and apply the above algorithm
we obtain the definition of ⊗cflat given above.  Similarly for ⊗cfringe.  

	There are other intensional properties of interest. For example
the number of calls ⊗flat makes to itself is given by 
.begin nofill turnon "∂" select 2 group
.n←20

∂(n)rflat[x, u] ← 
!fcnrflat& ∂(n+4)qif qat x qthen $1 
∂(n+4)qelse $1 + rflat[qa x, flat[qd x, u]] + rflat[qd x, u].
.end
Thus
.begin nofill

⊗⊗⊗rflat[$$(A . (B . (C . D)))$, qNIL] = $7 ⊗
⊗⊗⊗rflat[$$(((A . B) . C) . D)$, qNIL] = $7 ⊗.
.end

We can express ⊗rflat in terms of the size of the input by

!eqnrflatval ⊗⊗⊗∀x u: rflat[x, u] = $$2$q*size x - $$1$⊗.

The maximum depth of recursion occuring in a computation of ⊗flat is
given by
.begin nofill turnon "∂" select 2 group
.n←20

∂(n)dflat[x, u] ← 
!fcndflat& ∂(n+4)if qat x qthen $$0$
∂(n+4)qelse $1 + max[dflat[qa x, flat[qd x, u]], dflat[qd x, u]],
.end
so that
.begin nofill

⊗⊗⊗dflat[$$(A . (B . (C . D)))$, qNIL] = $3 ⊗
⊗⊗⊗dflat[$$((A . B) . (C . D))$, qNIL] = $2 ⊗
and
!eqndflatval ⊗⊗⊗∀x u: dflat[x, u] = $$length of longest qa - qd chain in$ x⊗.
.end

	A somewhat more complex property is the trace of the computation.  
A trace is a list of n+1-tuples (<arg1>...<argn> <result>) containing
one such tuple for each call to the function being traced.  Thus if we
wish to compute a trace of ⊗flat we can use ⊗tflat.  
.begin nofill turnon "∂" select 2 group
.n←20

∂(n)tflat[x, u] ← 
!fcntflat& ∂(n+4)qif qat x qthen <<x, u, flat[x, u]>>
∂(n+4)qelse <x, u, flat[x, u]> . [tflat[qd x, u] * tflat[qa x, flat[qd x, u]]]

.end
For example the traces of ⊗⊗flat[$$(A_B_C_._D),NIL$]⊗ and 
⊗⊗flat[$$(((A_._B)_._C)_._D),NIL$]⊗ are
.begin nofill group turnon "∂" select 6
.n←20 m←32

∂(n)	⊗⊗tflat⊗[(A . (B . (C . D))), qNIL] = 
∂(m-1)                 	      (((A B C . D) NIL (A B C D))
∂(m)			       ((B C . D) NIL (B C D))
∂(m)			       ((C . D) NIL (C D))
∂(m)			       (D NIL (D))
∂(m)			       (C (D) (C D))
∂(m)			       (B (C D) (B C D))
∂(m)			       (A (B C D) (A B C D)))
.apart 

.group
∂(n)	⊗⊗tflat⊗[(((A . B) . C) . D), qNIL] = 
∂(m-1)			      (((((A . B) . C) . D) NIL (A B C D))
∂(m)			       (D NIL (D))
∂(m)			       (((A . B) . C) (D) (A B C D))
∂(m)			       (C (D) (C D))
∂(m) 			       ((A . B) (C D) (A B C D))
∂(m)			       (B (C D) (B C D))
∂(m)			       (A (B C D) (A B C D))))
.end


The idea for general cost computing programs is due to Ben Moszkoswki.
This is described and many sample applications are given in Moszkowski[1978].

.skip 2
.if lines < 5 then next page
.cb Exercises
.item←0

#. Define functions to compute the number of ⊗⊗cons⊗es executed
by the programs ⊗reverse ({eqn reverse!!}) and ⊗reversea ({eqn reversea!!})
and work out the relation between these costs.


.ss(extendex,Substantial exercises)

.item←0
#. Write a program to convert functional LISP programs into iterative
(sequential) programs for some class of programs.

#. Implement the algorithm for producing cost computing derived functions
described in qsect{subsection derive}.

#. Write a program that transforms a program into one that computes the
trace of a functional LISP program.